Intersection Types for the Resource Control Lambda Calculi
Identifieur interne : 002678 ( Main/Exploration ); précédent : 002677; suivant : 002679Intersection Types for the Resource Control Lambda Calculi
Auteurs : Silvia Ghilezan [Serbie] ; Jelena Iveti [Serbie] ; Pierre Lescanne [France] ; Silvia Likavec [Italie]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: We propose intersection type assignment systems for two resource control term calculi: the lambda calculus and the sequent lambda calculus with explicit operators for weakening and contraction. These resource control calculi, λ ® and $\lambda_\circledR^{Gtz}$ , respectively, capture the computational content of intuitionistic natural deduction and intuitionistic sequent logic with explicit structural rules. Our main contribution is the characterisation of strong normalisation of reductions in both calculi. We first prove that typability implies strong normalisation in λ ® by adapting the reducibility method. Then we prove that typability implies strong normalisation in $\lambda_\circledR^{Gtz}$ by using a combination of well-orders and a suitable embedding of $\lambda_\circledR^{Gtz}$ -terms into λ ®-terms which preserves types and enables the simulation of all its reductions by the operational semantics of the λ ®-calculus. Finally, we prove that strong normalisation implies typability in both systems using head subject expansion.
Url:
DOI: 10.1007/978-3-642-23283-1_10
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 002546
- to stream Istex, to step Curation: 002515
- to stream Istex, to step Checkpoint: 000578
- to stream Main, to step Merge: 002720
- to stream Main, to step Curation: 002678
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Intersection Types for the Resource Control Lambda Calculi</title><author><name sortKey="Ghilezan, Silvia" sort="Ghilezan, Silvia" uniqKey="Ghilezan S" first="Silvia" last="Ghilezan">Silvia Ghilezan</name></author><author><name sortKey="Iveti, Jelena" sort="Iveti, Jelena" uniqKey="Iveti J" first="Jelena" last="Iveti">Jelena Iveti</name></author><author><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name><affiliation><country>France</country><placeName><settlement type="city">Lyon</settlement><region type="region" nuts="2">Rhône-Alpes</region></placeName><orgName type="universitySchool" n="3">École normale supérieure de Lyon</orgName></affiliation></author><author><name sortKey="Likavec, Silvia" sort="Likavec, Silvia" uniqKey="Likavec S" first="Silvia" last="Likavec">Silvia Likavec</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:9F456A0DD9008E357E2526063569782FC660552C</idno><date when="2011" year="2011">2011</date><idno type="doi">10.1007/978-3-642-23283-1_10</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-NCV35KMF-W/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002546</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002546</idno><idno type="wicri:Area/Istex/Curation">002515</idno><idno type="wicri:Area/Istex/Checkpoint">000578</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000578</idno><idno type="wicri:doubleKey">0302-9743:2011:Ghilezan S:intersection:types:for</idno><idno type="wicri:Area/Main/Merge">002720</idno><idno type="wicri:Area/Main/Curation">002678</idno><idno type="wicri:Area/Main/Exploration">002678</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Intersection Types for the Resource Control Lambda Calculi</title><author><name sortKey="Ghilezan, Silvia" sort="Ghilezan, Silvia" uniqKey="Ghilezan S" first="Silvia" last="Ghilezan">Silvia Ghilezan</name><affiliation wicri:level="1"><country xml:lang="fr">Serbie</country><wicri:regionArea>Faculty of Technical Sciences, University of Novi Sad</wicri:regionArea><wicri:noRegion>University of Novi Sad</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Serbie</country></affiliation></author><author><name sortKey="Iveti, Jelena" sort="Iveti, Jelena" uniqKey="Iveti J" first="Jelena" last="Iveti">Jelena Iveti</name><affiliation wicri:level="1"><country xml:lang="fr">Serbie</country><wicri:regionArea>Faculty of Technical Sciences, University of Novi Sad</wicri:regionArea><wicri:noRegion>University of Novi Sad</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Serbie</country></affiliation></author><author><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>École Normal Supérieure de Lyon, University of Lyon</wicri:regionArea><wicri:noRegion>University of Lyon</wicri:noRegion><wicri:noRegion>University of Lyon</wicri:noRegion><placeName><settlement type="city">Lyon</settlement><region type="region" nuts="2">Rhône-Alpes</region></placeName><orgName type="universitySchool" n="3">École normale supérieure de Lyon</orgName></affiliation></author><author><name sortKey="Likavec, Silvia" sort="Likavec, Silvia" uniqKey="Likavec S" first="Silvia" last="Likavec">Silvia Likavec</name><affiliation wicri:level="1"><country xml:lang="fr">Italie</country><wicri:regionArea>Dipartimento di Informatica, Università di Torino</wicri:regionArea><wicri:noRegion>Università di Torino</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Italie</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We propose intersection type assignment systems for two resource control term calculi: the lambda calculus and the sequent lambda calculus with explicit operators for weakening and contraction. These resource control calculi, λ ® and $\lambda_\circledR^{Gtz}$ , respectively, capture the computational content of intuitionistic natural deduction and intuitionistic sequent logic with explicit structural rules. Our main contribution is the characterisation of strong normalisation of reductions in both calculi. We first prove that typability implies strong normalisation in λ ® by adapting the reducibility method. Then we prove that typability implies strong normalisation in $\lambda_\circledR^{Gtz}$ by using a combination of well-orders and a suitable embedding of $\lambda_\circledR^{Gtz}$ -terms into λ ®-terms which preserves types and enables the simulation of all its reductions by the operational semantics of the λ ®-calculus. Finally, we prove that strong normalisation implies typability in both systems using head subject expansion.</div></front></TEI><affiliations><list><country><li>France</li><li>Italie</li><li>Serbie</li></country><region><li>Rhône-Alpes</li></region><settlement><li>Lyon</li></settlement><orgName><li>École normale supérieure de Lyon</li></orgName></list><tree><country name="Serbie"><noRegion><name sortKey="Ghilezan, Silvia" sort="Ghilezan, Silvia" uniqKey="Ghilezan S" first="Silvia" last="Ghilezan">Silvia Ghilezan</name></noRegion><name sortKey="Ghilezan, Silvia" sort="Ghilezan, Silvia" uniqKey="Ghilezan S" first="Silvia" last="Ghilezan">Silvia Ghilezan</name><name sortKey="Iveti, Jelena" sort="Iveti, Jelena" uniqKey="Iveti J" first="Jelena" last="Iveti">Jelena Iveti</name><name sortKey="Iveti, Jelena" sort="Iveti, Jelena" uniqKey="Iveti J" first="Jelena" last="Iveti">Jelena Iveti</name></country><country name="France"><region name="Rhône-Alpes"><name sortKey="Lescanne, Pierre" sort="Lescanne, Pierre" uniqKey="Lescanne P" first="Pierre" last="Lescanne">Pierre Lescanne</name></region></country><country name="Italie"><noRegion><name sortKey="Likavec, Silvia" sort="Likavec, Silvia" uniqKey="Likavec S" first="Silvia" last="Likavec">Silvia Likavec</name></noRegion><name sortKey="Likavec, Silvia" sort="Likavec, Silvia" uniqKey="Likavec S" first="Silvia" last="Likavec">Silvia Likavec</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002678 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 002678 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:9F456A0DD9008E357E2526063569782FC660552C
|texte= Intersection Types for the Resource Control Lambda Calculi
}}
| This area was generated with Dilib version V0.6.33. |  |